/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.gui;

import java.awt.event.ComponentAdapter;
import java.awt.event.ComponentEvent;
import java.awt.event.ComponentListener;
import java.util.ArrayList;
import java.util.Iterator;

import javax.swing.JComponent;
import javax.swing.JScrollPane;
import javax.swing.JTree;
import javax.swing.event.TreeExpansionEvent;
import javax.swing.event.TreeWillExpandListener;
import javax.swing.tree.DefaultTreeModel;
import javax.swing.tree.ExpandVetoException;
import javax.swing.tree.TreeNode;

import alloy.api.Atom;
import alloy.api.Instance;
import alloy.api.Relation;
import alloy.api.SolutionData;
import alloy.api.Tuple;
import alloy.ast.LeafExpr;
import alloy.ast.LeafId;
import alloy.ast.SigExpr;
import alloy.ast.Signature;
import alloy.type.BasicType;
import alloy.type.SigType;
import alloy.util.Dbg;

// SolutionTree represents the infinitely expanding value tree.

class SolutionTree extends GUITree {
    JTree valueTree;
    DefaultTreeModel valueTreeModel;
    AlloyGUITreeNode valueNode;
    ValueTreeWillExpandListener expansionListener;
    SolutionData solutionData;
    ArrayList modeList;
    JScrollPane valueScrollPane;

    Instance instance;

    SolutionTree() {
        valueNode = new AlloyGUITreeNode("Solution", true);
        valueNode.setName("Solution");

        valueTree = new JTree(valueNode, true);
        valueTree.putClientProperty("JTree.lineStyle", "Angled");
        valueTree.setRootVisible(true);
        valueScrollPane = new JScrollPane(valueTree);
        // JScrollPane.VERTICAL_SCROLLBAR_ALWAYS,
        // JScrollPane.HORIZONTAL_SCROLLBAR_ALWAYS);

        valueTreeModel = (DefaultTreeModel)valueTree.getModel();
        expansionListener = new ValueTreeWillExpandListener();
        valueTree.addTreeWillExpandListener(
            (TreeWillExpandListener)AlloySwingUtilities.listener(expansionListener));

        modeList = new ArrayList();

		// ugly fix for truncated nodes problem on mac...
		if (AlloySwingUtilities.onMac()) {
			ComponentListener nodeFixer = (ComponentListener)AlloySwingUtilities.listener(new ComponentAdapter() {
    	       		public void componentShown(ComponentEvent e) {
						valueTreeModel.reload();
						valueScrollPane.removeComponentListener(this);
		      		}
		      	});
	        valueScrollPane.addComponentListener(nodeFixer);
		}
    }

    public JComponent getComponent() {
        return valueScrollPane;
    }

    // When we first get the value-mapping data from the Analyzer, we
    // need to call this to set up the initial nodes that branch off of
    // the root node: the signature nodes.
    protected void setupSignatureNodes(SolutionData solutionData_) {
        /*
          Let us do this:
          -Get the names of all the signatures
          -create a node for each, with its "allows children" property set to true
          if it has any atoms in it.
          -add these nodes to the root value node.
          
          "Let's do this" revised (to use alloy.api.Instance):
          
        */
        solutionData = solutionData_;

        instance = (Instance)solutionData_;

        Dbg.chk(solutionData, "solutionData");
        Dbg.chk(solutionData.allSigs(), "solutionData.allSigs()");

        Iterator sigIterator = instance.getSigExprs().iterator();

        SigExpr sigExpr;
        String sigName;
        boolean hasAtoms;
        AlloyGUITreeNode newNode;
        int cntr = 0;
        for (; sigIterator.hasNext(); cntr++) {

            sigExpr = (SigExpr)sigIterator.next();
            sigName = instance.getShortSigName(sigExpr);
            if (instance.getRelation(sigExpr.getLeafId()).numberOfTuples() != 0)
                hasAtoms = true;
            else
                hasAtoms = false;

            newNode = new AlloyGUITreeNode(sigName, hasAtoms, AlloyGUITreeNode.SIGNATURE);
            newNode.setLeafExpr(sigExpr);
            valueTreeModel.insertNodeInto(newNode, valueNode, cntr);
        }

        // also add skolem constants
        Iterator skolemIter = instance.getSkolems().iterator();
        boolean hasTuples;
        for (; skolemIter.hasNext(); cntr++) {
            LeafExpr skolem = (LeafExpr)skolemIter.next();
            String skolemName = instance.shortenSkolem(skolem.nodeString());
            if (instance.getRelation(skolem.getLeafId()).numberOfTuples() != 0)
                hasTuples = true;
            else
                hasTuples = false;

            newNode = new AlloyGUITreeNode(skolemName, hasTuples, AlloyGUITreeNode.SKOLEM);
            newNode.setLeafExpr(skolem);
            valueTreeModel.insertNodeInto(newNode, valueNode, cntr);
        }

        valueTree.expandRow(0); //ensure the signatures are visible.
    }

    private AlloyGUITreeNode makeNewAtomNode(Atom atom) {

        boolean hasChildren;
        AlloyGUITreeNode newNode;

        String atomName = atom.toString();

		BasicType atomType = instance.getBasicTypeForAtom(atom);

		// Now I need to determine if the atom's signature has fields; if
		// so, then the node must be capable of having children.               
		if ((atomType instanceof SigType) && ((SigType)atomType).getSignature().getAllFieldNames().size() > 0)
			hasChildren = true;
		else
			hasChildren = false;

        newNode = new AlloyGUITreeNode(new String(atomName), hasChildren, AlloyGUITreeNode.ATOM);
        newNode.setAtom(atom);

        return newNode;
    }

    public void saveTreeMode() {
        saveTreeMode(valueTree, modeList, valueNode);
    }

    public void restoreTreeMode() {
        restoreTreeMode(valueTree, modeList, valueNode, true);
    }

    public void expandNode(AlloyGUITreeNode node) {
        TreeNode[] treePath = node.getPath();

        if (node.alreadyExpanded()) {
            return;
        } else {
            int nodeType = node.getNodeType();

            if (nodeType == AlloyGUITreeNode.SIGNATURE) {
                // we need to look up the atoms contained in this signature's set
                // and add them to the parent node.

                Relation rel = instance.getRelation(node.getLeafExpr().getLeafId());
                String atomName;
                AlloyGUITreeNode newNode;

                int cntr = 0;
                for (Iterator tupIter = rel.tuples(); tupIter.hasNext();) {
                    Tuple tup = (Tuple)tupIter.next();
                    Atom atom = (Atom)tup.atoms().next();
                    newNode = makeNewAtomNode(atom);
                    valueTreeModel.insertNodeInto(newNode, node, cntr);
                    cntr++;
                }

            } else if (nodeType == AlloyGUITreeNode.ATOM) {
				// First, we need to get the atom's type. Then, we check if that type
				// has fields--if so, add them to the parent.

               
				AlloyGUITreeNode newNode;

				BasicType atomType = instance.getBasicTypeForAtom(node.getAtom());
                
				if (atomType instanceof SigType) {                
                	
				Signature sig = ((SigType)atomType).getSignature();
				Iterator fieldIterator = sig.getAllFieldNames().iterator(); //instance.getFieldExprsForAtom(node.getAtom()).iterator();

				for (int cntr = 0; fieldIterator.hasNext(); cntr++) {
					String fieldName = (String)fieldIterator.next();
					LeafId fieldId = sig.searchFieldLeafIdUpwards(fieldName); 
					LeafExpr fieldExpr = new alloy.ast.VariableExpr(new alloy.ast.Variable(new alloy.ast.Id(fieldName)));
					fieldExpr.setType(sig.searchFieldTypeUpwards(fieldName));
					fieldExpr.setLeafId(fieldId);
                	
                    
					// All fields have values (not necessarily!)
					// and thus, all these nodes will
					// have children.

					// We check if the relation has any members.                    
					int numMembers =
						instance.applyFieldToAtom(fieldId, node.getAtom()).numberOfTuples();

					newNode =
						new AlloyGUITreeNode(
							new String(fieldName),
							(numMembers != 0),
							AlloyGUITreeNode.FIELD);
					newNode.setLeafExpr(fieldExpr);
					valueTreeModel.insertNodeInto(newNode, node, cntr);
				}
                
				}
            } else if (nodeType == AlloyGUITreeNode.FIELD) {
                // A "FIELD" type indicates that this is a field of an atom; so what we
                // need to do is look up what the field of this atom is mapped to.

                Atom atom;
                String fieldName, atomName;
                AlloyGUITreeNode atomNode;
                AlloyGUITreeNode newNode;

                fieldName = node.getName();
                atomNode = (AlloyGUITreeNode)treePath[treePath.length - 2];
                atomName = atomNode.getName();
                atom = atomNode.getAtom();
                Relation fieldValues = instance.applyFieldToAtom(node.getLeafExpr().getLeafId(), atom);
                Iterator tupleIter = fieldValues.tuples();

                // Here we iterate over all the tuple mappings.
                for (int cntr = 0; tupleIter.hasNext(); cntr++) {
                    Tuple fieldTuple = (Tuple)tupleIter.next();

                    if (fieldTuple.arity()== 1) {
                        //This is a simple atom relation, and needs no additional expansion.
                        newNode = makeNewAtomNode((Atom)fieldTuple.atoms().next());
                        valueTreeModel.insertNodeInto(newNode, node, cntr);
                    } else {
                        // And here we iterate over all n atoms in the n-tuple
                        AlloyGUITreeNode tupleNode;

                        Iterator atomIter = fieldTuple.atoms();                        
                        String newNodeName = ((Atom)atomIter.next()).toString();
                        while (atomIter.hasNext()) {                        
                            newNodeName = newNodeName.concat("->" + ((Atom)atomIter.next()).toString());
                        }

                        tupleNode =
                            new AlloyGUITreeNode(
                                new String(newNodeName),
                                true,
                                AlloyGUITreeNode.TUPLE);
                        valueTreeModel.insertNodeInto(tupleNode, node, cntr);
                        
                        int tuple_cntr = 0;
                        atomIter = fieldTuple.atoms();
                        while (atomIter.hasNext()) {                        
                            newNode = makeNewAtomNode((Atom)atomIter.next());
                            valueTreeModel.insertNodeInto(newNode, tupleNode, tuple_cntr);
							tuple_cntr++;
                        }
                        tupleNode.setExpanded(true);
                    } //end else this is an n-tuple
                } //end for loop over the field iterator
            } //end if this is a field node
            else if (nodeType == AlloyGUITreeNode.SKOLEM) {
                // a "SKOLEM" node type indicates this node represents a skolem constant.
                // handled similarly to field

                String skolemName = node.getLeafExpr().nodeString();                
                Relation skolemValues = instance.getRelation(node.getLeafExpr().getLeafId());;
				Tuple skolemTuple;
                AlloyGUITreeNode newNode;
                                
                Iterator tupleIter = skolemValues.tuples();

                // Here we iterate over all the tuple mappings.
                for (int cntr = 0; tupleIter.hasNext(); cntr++) {
                    skolemTuple = (Tuple)tupleIter.next();

                    if (skolemTuple.arity() == 1) {
                        //This is a simple atom relation, and needs no additional expansion.
                        newNode = makeNewAtomNode((Atom)skolemTuple.atoms().next());
                        valueTreeModel.insertNodeInto(newNode, node, cntr);
                    } else {
                        // And here we iterate over all n atoms in the n-tuple
                        AlloyGUITreeNode tupleNode;

						Iterator atomIter = skolemTuple.atoms();
                        String newNodeName = ((Atom)atomIter.next()).toString();
                        int ncntr = 1;
                        while (atomIter.hasNext()) {                                                
                            newNodeName = newNodeName.concat("->" + ((Atom)atomIter.next()).toString());
							ncntr++;
                        }

                        tupleNode =
                            new AlloyGUITreeNode(
                                new String(newNodeName),
                                true,
                                AlloyGUITreeNode.TUPLE);
                        valueTreeModel.insertNodeInto(tupleNode, node, cntr);
                        
                        atomIter = skolemTuple.atoms();
                        for (int tuple_cntr = 0; atomIter.hasNext(); tuple_cntr++) {
                            newNode = makeNewAtomNode((Atom)atomIter.next());
                            valueTreeModel.insertNodeInto(newNode, tupleNode, tuple_cntr);
                        }
                        tupleNode.setExpanded(true);
                    } //end else this is an n-tuple
                } //end for loop over the skolem iterator
            } //end if this is a skolem node

            else if (nodeType == AlloyGUITreeNode.OTHER) {
                // Don't do anything, yo.
            } else {
                Dbg.warn(
                    "We have encountered a AlloyGUITreeNode with an improper type.\n");
            }

            node.setExpanded(true);
        }
    } //end expandNode

    public void clearTree() {
        valueNode.removeAllChildren();
        valueTreeModel.nodeStructureChanged(valueNode);
    }

    JTree[] getTrees() {
        JTree[] trees = new JTree[1];
        trees[0] = valueTree;
        return trees;
    }

    // This will do all the work of generating our infinite value-mapping tree.
    protected class ValueTreeWillExpandListener implements TreeWillExpandListener {
        public void treeWillCollapse(TreeExpansionEvent treeExpansionEvent)
            throws ExpandVetoException {
        }

        public void treeWillExpand(TreeExpansionEvent treeWillExpand) throws ExpandVetoException {
            AlloyGUITreeNode node =
                (AlloyGUITreeNode)treeWillExpand.getPath().getLastPathComponent();
            expandNode(node);
        }
    }

}
